\documentclass[DaoFP]{subfiles}
\begin{document}
\setcounter{chapter}{3}

\chapter{Sum Types}

\section{Bool}

We know how to compose arrows. But how do we compose objects?

 We have defined $0$ (the initial object) and $1$ (the terminal object). What is $2$ if not $1$ plus $1$?
 
A $2$ is an object with two elements: two arrows coming from $1$. Let's call one arrow \hask{True} and the other \hask{False}. Don't confuse those names with the logical interpretations of the initial and the terminal objects. These two are \emph{arrows}. 

\[
 \begin{tikzcd}
 1
 \arrow[dd, bend right, "\text{True}"']
 \arrow[dd, bend left, "\text{False}"]
 \\
 \\
2
 \end{tikzcd}
\]

This simple idea can be immediately expressed in Haskell\footnote{This style of definition is called the Generalized Algebraic Data Types or \hask{GADTs} in Haskell} as the definition of a type, traditionally called \hask{Bool}, after its inventor George Boole (1815-1864).

\begin{haskell}
data Bool where
  True  :: () -> Bool
  False :: () -> Bool
\end{haskell}
It corresponds to the same diagram (only with some Haskell renamings):
\[
 \begin{tikzcd}
 \hask{()}
 \arrow[dd, bend right, "\hask{True}"']
 \arrow[dd, bend left, "\hask{False}"]
 \\
 \\
\hask{Bool}
 \end{tikzcd}
\]

As we've seen before, there is a shortcut notation for elements, so here's a more compact version:

\begin{haskell}
data Bool where
  True  :: Bool
  False :: Bool
\end{haskell}

We can now define a term of the type \hask{Bool}, for instance
\begin{haskell}
x :: Bool
x = True
\end{haskell}
The first line declares \hask{x} to be an element of \hask{Bool} (secretly a function \hask{()->Bool}), and the second line tells us which one of the two.

The functions \hask{True} and \hask{False} that we used in the definition of \hask{Bool} are called \index{data constructor}\emph{data constructors}. They can be used to construct specific terms, like in the example above. As a side note, in Haskell, function names start with lower-case letters, except when they are data constructors. 

Our definition of the type \hask{Bool} is still incomplete. We know how to construct a \hask{Bool} term, but we don't know what to do with it. We have to be able to define arrows that go out of \hask{Bool}---the \index{mapping out}\emph{mappings ou}t of \hask{Bool}. 

The first observation is that, if we have an arrow \hask{h} from \hask{Bool} to some concrete type \hask{A} then we automatically get two arrows \hask{x} and \hask{y} from unit to \hask{A}, just by composition. The following two (distorted) triangles commute:

\[
 \begin{tikzcd}
 \hask{()}
 \arrow[dd, bend right, "\text{True}"']
 \arrow[dd, bend left, "\text{False}"]
  \arrow[ddd, bend right =90, "x"']
 \arrow[ddd, bend left=90, "y"]
\\
 \\
\text{Bool}
\arrow[d, dashed, "h"]
\\
A
 \end{tikzcd}
\]
In other words, every function \hask{Bool->A} produces a pair of elements of \hask{A}.

Given a concrete type \hask{A}:
\begin{haskell}
h :: Bool -> A
\end{haskell}
we have:
\begin{haskell}
x = h True
y = h False
\end{haskell}
where
\begin{haskell}
x :: A
y :: A
\end{haskell}
Notice the use of the shorthand notation for the application of a function to an element:
\begin{haskell}
h True -- meaning: h . True
\end{haskell}

We are now ready to complete our definition of \hask{Bool} by adding the condition that any function from \hask{Bool} to \hask{A} not only produces but \emph{is equivalent} to a pair of elements of \hask{A}. In other words, a pair of elements uniquely determines a function from \hask{Bool}. 

What this means is that we can interpret the diagram above in two ways: Given \hask{h}, we can easily get \hask{x} and \hask{y}. But the converse is also true: a pair of elements \hask{x} and \hask{y} uniquely \emph{defines} \hask{h}.

We have a bijection at work here. This time it's a one-to-one mapping between a pair of elements $(x, y)$ and an arrow $h$. 

In Haskell, this definition of \hask{h} is encapsulated in the \index{\hask{if} statement}\hask{if}, \hask{then}, \hask{else} construct. Given
\begin{haskell}
x :: A
y :: A
\end{haskell}
we define the mapping out
\begin{haskell}
h :: Bool -> A
h b = if b then x else y
\end{haskell}
Here, \hask{b} is a term of the type \hask{Bool}. 

In general, a data type is created using \index{introduction rule}\emph{introduction} rules and deconstructed using \index{elimination rule}\emph{elimination} rules. The \hask{Bool} data type has two introduction rules, one using \hask{True} and another using \hask{False}. The \hask{if}, \hask{then}, \hask{else} construct defines the elimination rule. 

The fact that, given the above definition of \hask{h}, we can retrieve the two terms that were used to define it, is called the \index{computation rule}\emph{computation} rule. It tells us how to compute the result of \hask{h}. If we call \hask{h} with \hask{True}, the result is \hask{x}; if we call it with \hask{False}, the result is \hask{y}.

We should never lose sight of the purpose of programming: to decompose complex problems into a series of simpler ones. The definition of \hask{Bool} illustrates this idea. Whenever we have to construct a mapping out of \hask{Bool}, we decompose it into two smaller tasks of constructing a pair of elements of the target type. We traded one larger problem for two simpler ones.

\subsection{Examples}

Let's do a few examples. We haven't defined many types yet, so we'll be limited to mappings out of \hask{Bool} to either \hask{Void}, \hask{()}, or \hask{Bool}. Such edge cases, however, may offer new insights into well known results.

We have decided that there can be no functions (other than identity) with \hask{Void} as a target, so we don't expect any functions from \hask{Bool} to \hask{Void}. And indeed, we have zero pairs of elements of \hask{Void}. 

What about functions from \hask{Bool} to \hask{()}? Since \hask{()} is terminal, there can be only one function from \hask{Bool} to it. And, indeed, this function corresponds to the single possible pair of functions from \hask{()} to \hask{()}---both being identities. So far so good.
\[
 \begin{tikzcd}
 \hask{()}
 \arrow[dd, bend right, "\text{True}"']
 \arrow[dd, bend left, "\text{False}"]
  \arrow[ddd, bend right =90, "\hask{id}"']
 \arrow[ddd, bend left=90, "\hask{id}"]
\\
 \\
\text{Bool}
\arrow[d, dashed, "h"]
\\
\hask{()}
 \end{tikzcd}
\]


The interesting case is functions from \hask{Bool} to \hask{Bool}. Let's plug \hask{Bool} in place of \hask{A}:
\[
 \begin{tikzcd}
 \hask{()}
 \arrow[dd, bend right, "\text{True}"']
 \arrow[dd, bend left, "\text{False}"]
  \arrow[ddd, bend right =90, "x"']
 \arrow[ddd, bend left=90, "y"]
\\
 \\
\text{Bool}
\arrow[d, dashed, "h"]
\\
\text{Bool}
 \end{tikzcd}
\]
How many pairs $(x, y)$ of functions from \hask{()} to \hask{Bool} do we have at our disposal? There are only two such functions, \hask{True} and \hask{False}, so we can form four pairs. These are $(True, True)$, $(False, False)$, $(True, False)$, and $(False, True)$. Therefore there can only be four functions from \hask{Bool} to \hask{Bool}. 

We can write them in Haskell using the  \hask{if}, \hask{then}, \hask{else} construct. For instance, the last one, which we'll call \hask{not} is defined as:
\begin{haskell}
not :: Bool -> Bool
not b = if b then False else True
\end{haskell}

We can also look at functions from \hask{Bool} to \hask{A} as elements of the object of arrows, or the exponential object $A^2$, where $2$ is the \hask{Bool} object. According to our count, we have zero elements in $0^2$, one element in $1^2$, and four elements in $2^2$. This is exactly what we'd expect from high-school algebra, where numbers actually mean numbers.

\begin{exercise}
Write the implementations of the three other functions \hask{Bool->Bool}.
\end{exercise}

\section{Enumerations}

What comes after 0, 1, and 2? An object with three data constructors. For instance:
\begin{haskell}
data RGB where
  Red   :: RGB
  Green :: RGB
  Blue  :: RGB
\end{haskell}
If you're tired of redundant syntax, there is a shorthand for this type of definition:

\begin{haskell}
data RGB = Red | Green | Blue
\end{haskell}
This introduction rule allows us to construct terms of the type \hask{RGB}, for instance:
\begin{haskell}
c :: RGB
c = Blue
\end{haskell}
To define mappings out of \hask{RGB}, we need a more general elimination pattern. Just like a function from \hask{Bool} was determined by two elements, a function from \hask{RGB} to \hask{A} is determined by a triple of elements of \hask{A}: \hask{x}, \hask{y}, and \hask{z}. We write such a function using \emph{pattern matching} syntax:
\begin{haskell}
h :: RGB -> A
h Red   = x
h Green = y
h Blue  = z
\end{haskell}
This is just one function whose definition is split into three cases. 

It's possible to use the same syntax for \hask{Bool} as well, in place of \hask{if}, \hask{then}, \hask{else}:
\begin{haskell}
h :: Bool -> A
h True  = x
h False = y
\end{haskell}
In fact, there is a third way of writing the same thing using the \index{\hask{case} statement}\hask{case} statement:
\begin{haskell}
h c = case c of
  Red   -> x
  Green -> y
  Blue  -> z
\end{haskell}
or even
\begin{haskell}
h :: Bool -> A
h b = case b of
  True  -> x
  False -> y
\end{haskell}
You can use any of these at your convenience when programming.

These patterns will also work for types with four, five, and more data constructors. For instance, a decimal digit is one of:
\begin{haskell}
data Digit = Zero | One | Two | Three | ... | Nine
\end{haskell}

There is a giant enumeration of Unicode characters called \hask{Char}. Their constructors are given special names: you write the character itself between two apostrophes, e.g.,
\begin{haskell}
c :: Char
c = 'a'
\end{haskell}

As Lao Tzu would say, a pattern of ten thousand things would take many years to complete, therefore people came up with the wildcard pattern, the underscore, which matches everything. 

Because the patterns are matched in order, you should use the wildcard pattern as the last one in a series:
\begin{haskell}
yesno :: Char -> Bool
yesno c = case c of
  'y' -> True
  'Y' -> True
  _   -> False
\end{haskell}

But why should we stop at that? The type \hask{Int} could be thought of as an enumeration of integers in the range between $-2^{29}$ and $2^{29}$ (or more, depending on the implementation). Of course, exhaustive pattern matching on such ranges is out of the question, but the principle holds. 

In practice, the types \hask{Char} for Unicode characters, \hask{Int} for fixed-precision integers, \hask{Double} for double-precision floating point numbers, and several others, are built into the language.

These are not infinite types. Their elements can be enumerated, even if it would take ten thousand years. The type \hask{Integer} is infinite, though.


\section{Sum Types}

The \hask{Bool} type could be seen as the sum $2 = 1 + 1$. But nothing stops us from replacing $1$ with another type, or even replacing each of the $1$s with different types. We can define a new type $a + b$ by using two arrows. Let's call them \hask{Left} and \hask{Right}. The defining diagram is the introduction rule:
\[
 \begin{tikzcd}
 a
 \arrow[dr,  "\text{Left}"']
 && b
 \arrow[dl, "\text{Right}"]
 \\
&a + b
 \end{tikzcd}
\]
In Haskell, the type $a + b$ is called \hask{Either a b}. By analogy with \hask{Bool}, we can define it as
\begin{haskell}
data Either a b where
  Left  :: a -> Either a b
  Right :: b -> Either a b
\end{haskell}
 (Note the use of lower-case letters for type variables.)
 
Similarly, the mapping out from $a + b$ to some type $c$ is determined by this commuting diagram:
\[
 \begin{tikzcd}
 a
 \arrow[dr,  bend left, "\text{Left}"']
 \arrow[ddr, bend right, "f"']
 && b
 \arrow[dl, bend right, "\text{Right}"]
 \arrow[ddl, bend left, "g"]
 \\
&a + b
\arrow[d, dashed, "h"]
\\
& c
 \end{tikzcd}
\]
Given a function $h$, we get a pair of functions $f$ and $g$ just by composing it with \hask{Left} and \hask{Right}. Conversely, such a pair of functions uniquely determines $h$. This is the elimination rule.

When we want to translate this diagram to Haskell, we need to select elements of the two types. We can do it by defining the arrows $a$ and $b$ from the terminal object. 
\[
 \begin{tikzcd}
 &1
 \arrow[ld, "a"']
 \arrow[rd, "b"]
 \\
 a
 \arrow[dr,  bend left, "\text{Left}"']
 \arrow[ddr, bend right, "f"']
 && b
 \arrow[dl, bend right, "\text{Right}"]
 \arrow[ddl, bend left, "g"]
 \\
&a + b
\arrow[d, dashed, "h"]
\\
& c
 \end{tikzcd}
\]
Follow the arrows in this diagram to get:
\[h \circ \text{Left} \circ a = f \circ a\]
\[h \circ \text{Right} \circ b = g \circ b\]

Haskell syntax repeats these equations almost literally, resulting in this pattern-matching syntax for the definition of \hask{h}:

\begin{haskell}
h :: Either a b -> c
h (Left  a) = f a
h (Right b) = g b
\end{haskell}
(Again, notice the use of lower-case letters for type variables and the same letters for terms of that type. Unlike humans, the compilers don't get confused by this.)

You can also read these equations right to left, and you will see the computation rules for sum types: The two functions that were used to define \hask{h} can be recovered by applying \hask{h} to \hask{(Left a)} and \hask{(Right b)}. 

You can also use the \hask{case} syntax to define \hask{h}:
\begin{haskell}
h e = case e of
  Left  a -> f a
  Right b -> g b
\end{haskell}

So what is the essence of a data type? It is but a recipe for manipulating arrows.

\subsection{Maybe}

A very useful data type, \hask{Maybe} is defined as a sum $1 + a$, for any $a$. This is its definition in Haskell:
\begin{haskell}
data Maybe a where
  Nothing :: () -> Maybe a
  Just    ::  a -> Maybe a
\end{haskell}
The data constructor \hask{Nothing} is an arrow from the unit type, and \hask{Just} constructs \hask{Maybe a} from \hask{a}. \hask{Maybe a} is isomorphic to \hask{Either () a}. It can also be defined using the shorthand notation
\begin{haskell}
data Maybe a = Nothing | Just a
\end{haskell}

\hask{Maybe} is mostly used to encode the return type of partial functions: ones that are undefined for some values of their arguments. In that case, instead of failing, such functions return \hask{Nothing}. In other programming languages partial functions are often implemented using exceptions (or core dumps).

\subsection{Logic}

In logic, the proposition $A + B$ is called the \index{alternative}alternative, or \emph{logical or}. You can prove it by providing the proof of $A$ or the proof of $B$. Either one will suffice. 

If you want to prove that $C$ follows from $A+B$, you have to be prepared for two eventualities: either somebody proved $A+B$ by proving $A$ (and $B$ could be false) or by proving $B$ (and $A$ could be false). In the first case, you have to show that $C$ follows from $A$. In the second case you need a proof that $C$ follows from $B$. These are exactly the arrows in the elimination rule for $A+B$.

\section{Cocartesian Categories}

In Haskell, we can define a sum of any two types using \hask{Either}. A category in which all sums exist, and the initial object exists, is called \emph{cocartesian}, and the sum is called a \emph{coproduct}. You might have noticed that sum types mimic addition of numbers. It turns out that the initial object plays the role of zero. 



\subsection{One Plus Zero}
Let's first show that $1 + 0 \cong 1$, meaning the sum of the terminal object and the initial object is isomorphic to the terminal object. The standard procedure for this kind of proofs is to use the Yoneda trick. Since sum types are defined by mapping out, we should compare arrows coming \emph{out} of either side. 

The Yoneda argument says that two objects are isomorphic if there is a bijection $\beta_a$ between the sets of arrows coming out of them to an arbitrary object $a$, and this bijection is natural.  
 
Let's look at the definition of $1 + 0$ and it's mapping out to any object $a$. This mapping is defined by a pair $(x, \mbox{!`})$, where $x$ is an element of $a$ and $\mbox{!`}$ is the unique arrow from the initial object to $a$ (the \hask{absurd} function in Haskell). 

\[
 \begin{tikzcd}
 1
 \arrow[dr,  bend left, "\text{Left}"']
 \arrow[ddr, bend right, "x"']
 && 0
 \arrow[dl, bend right, "\text{Right}"]
 \arrow[ddl, bend left, "\mbox{!`}"]
 \\
&1 + 0
\arrow[d, dashed, "h"]
\\
& a
 \end{tikzcd}
 \qquad
 \begin{tikzcd}
 1
 \arrow[dd, "x"]
 \\
 \\
 a
 \end{tikzcd}
\]
We want to establish a one-to-one mapping between arrows originating in $1+0$ and the ones originating in $1$. The arrow $h$ is determined by the pair $(x, \mbox{!`})$. Since there is only one $\mbox{!`}$, there  is a bijection between $h$'s and $x$'s. 

We define $\beta_a$ to map any $h$ defined by a pair $(x, \mbox{!`})$ to $x$. Conversely, $\beta^{-1}_a$ maps $x$ to the pair $(x, \mbox{!`})$. But is it a natural transformation? 

To answer that, we need to consider what happens when we change focus from $a$ to some $b$ that is connected to it through an arrow $g \colon a \to b$. We have two options now:
\begin{itemize}
\item Make $h$ switch focus by post-composing both $x$ and $\mbox{!`}$ with $g$. We get a new pair $(y = g \circ x, \mbox{!`})$. Follow it by $\beta_b$.
\item Use $\beta_a$ to map $(x, \mbox{!`})$ to $x$. Follow it with the post-composition $(g \circ -)$. 
\end{itemize}
In both cases we get the same arrow $y = g \circ x$. So the mapping $\beta$ is natural. Therefore $1 + 0$ is isomorphic to $1$.

In Haskell, we can define the two functions that form the isomorphism, but there is no way of directly expressing the fact that they are the inverse of each other.
\begin{haskell}
f :: Either () Void -> ()
f (Left ()) = ()
f (Right _) = ()

f_1 :: () -> Either () Void
f_1 _ = Left ()
\end{haskell}
The underscore wildcard in a function definition means that the argument is ignored. The second clause in the definition of \hask{f} is redundant, since there are no terms of the type \hask{Void}. 

\subsection{Something Plus Zero}
A very similar argument can be used to show that $a + 0 \cong a$. The following diagram explains it.
\[
 \begin{tikzcd}
 a
 \arrow[dr,  bend left, "\text{Left}"']
 \arrow[ddr, bend right, "f"']
 && 0
 \arrow[dl, bend right, "\text{Right}"]
 \arrow[ddl, bend left, "\mbox{!`}"]
 \\
&a + 0
\arrow[d, dashed, "h"]
\\
& x
 \end{tikzcd}
 \qquad
 \begin{tikzcd}
 a
 \arrow[dd, "f"]
 \\
 \\
 x
 \end{tikzcd}
\]

We can translate this argument to Haskell by implementing a (polymorphic) function \hask{h} that works for any type \hask{a}. 

\begin{exercise}
Implement, in Haskell, the two functions that form the isomorphism between \hask{(Either a Void)} and \hask{a}.
\end{exercise}

We could use a similar argument to show that $0 + a \cong a$, but there is a more general property of sum types that obviates that.
\subsection{Commutativity}

There is a nice left-right symmetry in the diagrams that define the sum type, which suggests that it satisfies the commutativity rule, $a + b \cong b + a$. 

Let's consider mappings out of both sides of this formula. You can easily see that, for every $h$ that is determined by a pair $(f, g)$ on the left, there is a corresponding $h'$ given by a pair $(g, f)$ on the right. That establishes the bijection of arrows.

\[
 \begin{tikzcd}
 a
 \arrow[dr,  bend left, "\text{Left}"']
 \arrow[ddr, bend right, "f"']
 && b
 \arrow[dl, bend right, "\text{Right}"]
 \arrow[ddl, bend left, "g"]
 \\
&a + b
\arrow[d, dashed, "h"]
\\
& x
 \end{tikzcd}
 \qquad
 \begin{tikzcd}
 b
 \arrow[dr,  bend left, "\text{Left}"']
 \arrow[ddr, bend right, "g"']
 && a
 \arrow[dl, bend right, "\text{Right}"]
 \arrow[ddl, bend left, "f"]
 \\
&b + a
\arrow[d, dashed, "h'"]
\\
& x
 \end{tikzcd}
\]

\begin{exercise}
Show that the bijection defined above is natural. Hint: Both $f$ and $g$ change focus by post-composition with $k \colon x \to y$.
\end{exercise}
\begin{exercise}
Implement, in Haskell, the function that witnesses the isomorphism between \hask{(Either a b)} and \hask{(Either b a)}. Notice that this function is its own inverse.
\end{exercise}

\subsection{Associativity}

Just like in arithmetic, the sum that we have defined is associative:
\[(a + b) + c \cong a + (b + c) \]
It's easy to write the mapping out for the left-hand side:
\begin{haskell}
h :: Either (Either a b) c -> x
h (Left (Left a))  = f1 a
h (Left (Right b)) = f2 b
h (Right c)        = f3 c
\end{haskell}
Notice the use of nested patterns like \hask{(Left (Left a))}, etc. The mapping is fully defined by a triple of functions. The same functions can be used to define the mapping out of the right-hand side:
\begin{haskell}
h' :: Either a (Either b c) -> x
h' (Left a)          = f1 a
h' (Right (Left b))  = f2 b
h' (Right (Right c)) = f3 c
\end{haskell}
This establishes a one-to-one mapping between triples of functions that define the two mappings out. This mapping is natural because all changes of focus are done using post-composition. Therefore the two sides are isomorphic.

This code can also be displayed in diagrammatical form. Here's the diagram for the left hand side of the isomorphism:
\[
 \begin{tikzcd}
 a
 \arrow[rd, "L"']
 \arrow[rrddd, bend right, red, "f_1"']
 && b
 \arrow[ld, "R"]
 \arrow[ddd, bend left=60, red, "f_2"]
&&c
 \arrow[lldd, "R"]
 \arrow[llddd, bend left, red, "f_3"]
 \\
 & a + b
  \arrow[rd, "L"']
 \\
&&(a + b) + c
 \arrow[d, dashed, "h"]
\\
&& x
 \end{tikzcd}
\]
\subsection{Functoriality}
Since the sum is defined by the mapping out property, it was easy to see what happens when we change focus: it changes ``naturally'' with the foci of the arrows that define the product. But what happens when we move the sources of those arrows? 

Suppose that we have arrows that map $a$ and $b$ to some $a'$ and $b'$:
\begin{align*}f &\colon a \to a' \\
g &\colon b \to b' 
\end{align*}
The composition of these arrows with the constructors $\text{Left}$ and $\text{Right}$, respectively, can be used to define the mapping between the sums:
\[
 \begin{tikzcd}
 a
 \arrow[d, "f"]
 \arrow[dr,  bend left, "\text{Left}"']
  && b
 \arrow[d, "g"]
 \arrow[dl, bend right, "\text{Right}"]
 \\
 a'
 \arrow[rd, "\text{Left}"']
&a + b
\arrow[d, dashed, "h"]
& b'
\arrow[ld, "\text{Right}"]
\\
& a' + b'
 \end{tikzcd}
\]
The pair of arrows, $(\text{Left} \circ f, \text{Right} \circ g)$ uniquely defines the arrow $h \colon a + b \to a' + b'$. The notation for this arrow is:
\[ a + b \xrightarrow{\langle f, g \rangle} a' + b' \]

This property of lifting a pair of arrows to act on the sum is called the \emph{functoriality} of the sum. You can imagine it as allowing you to transform the two objects \emph{inside} the sum and get a new sum. 
\begin{exercise}
Show that functoriality preserves composition. Hint: take two composable arrows, $g \colon b \to b'$ and $g' \colon b' \to b''$ and show that applying $g' \circ g$ gives the same result as first applying $g$ to transform $a + b$ to $a + b'$ and then applying $g'$ to transform $a + b'$ to $a + b''$.
\end{exercise}

\begin{exercise}
Show that functoriality preserves identity. Hint: use $id_b$ and show that it is mapped to $id_{a+b}$.
\end{exercise}

\subsection{Symmetric Monoidal Category}
When a child learns addition we call it arithmetic. When a grownup learns addition we call it a cocartesian category.

Whether we are adding numbers, composing arrows, or constructing sums of objects, we are re-using the same idea of decomposing complex things into their simpler components.  

As Lao Tzu would say, when things come together to form a new thing, and the operation is associative, and it has a neutral element, we know how to deal with ten thousand things.

The sum type we have defined satisfies these properties:
\begin{align*}
a + 0 &\cong a \\
a + b &\cong b + a \\
(a + b) + c &\cong a + (b + c)
\end{align*}
and it's functorial. A category with this type of operation is called \emph{symmetric monoidal}. When the operation is the sum (coproduct), it's called \emph{cocartesian}. In the next chapter we'll see another monoidal structure that's called \emph{cartesian} without the ``co.''


\end{document}
